f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)
↳ QTRS
↳ DependencyPairsProof
f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)
F1(h2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(y)
F1(g2(x, y)) -> G2(f1(x), f1(y))
F1(h2(x, y)) -> G2(h2(y, f1(x)), h2(x, f1(y)))
F1(g2(x, y)) -> F1(x)
F1(h2(x, y)) -> F1(x)
f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F1(h2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(y)
F1(g2(x, y)) -> G2(f1(x), f1(y))
F1(h2(x, y)) -> G2(h2(y, f1(x)), h2(x, f1(y)))
F1(g2(x, y)) -> F1(x)
F1(h2(x, y)) -> F1(x)
f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
F1(h2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(x)
F1(h2(x, y)) -> F1(x)
f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F1(h2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(y)
F1(g2(x, y)) -> F1(x)
F1(h2(x, y)) -> F1(x)
POL( F1(x1) ) = max{0, 2x1 - 1}
POL( g2(x1, x2) ) = 2x1 + 2x2 + 2
POL( h2(x1, x2) ) = 2x1 + 2x2 + 2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f1(a) -> b
f1(c) -> d
f1(g2(x, y)) -> g2(f1(x), f1(y))
f1(h2(x, y)) -> g2(h2(y, f1(x)), h2(x, f1(y)))
g2(x, x) -> h2(e, x)